(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun g () String)
(assert (= "-" (str.substr a (str.len d) (str.len f))))
(assert (= (ite (= (str.substr a 0 (str.len d)) "proxyauthenticate") 1 0) (ite (= (str.substr a 0 (str.len d)) "keepalive") 1 0) (ite (= d "connection") 1 0) (ite (= (str.at (str.substr c 0 (str.len e)) (- (str.len e) 1)) "\u;") 1 0) (ite (= (str.at e (- (str.len (str.substr c 0 (str.len e))) 1)) "\ud") 1 0) (ite (= (str.at e (- (str.len e) 1)) "\ua") 1 0) (ite (= (str.at (str.substr c 0 (str.len e)) (- (str.len (str.substr c 0 (str.len e))) 1)) "\u9") 1 0) (ite (= (str.at e (- (str.len (str.substr c 0 (str.len e))) 1)) " ") 1 0) (ite (= (str.at e 0) "\u") 1 0) (ite (= (str.at (str.substr c 0 (str.len e)) 0) "\u") 1 0) (ite (= (str.at (str.substr c 0 (str.len e)) 0) "\u;") 1 0) (ite (= (str.at (str.substr c 0 (str.len e)) 0) "\ua") 1 0) (ite (= (str.at (str.substr c 0 (str.len e)) 0) "\u9") 1 0) (ite (= (str.at e 0) " ") 1 0) (ite (str.contains (str.substr c 0 (str.len e)) ",") 1 0) (ite (= (str.len e) 0) 1 0) 0))
(assert (= (str.substr b 0 (str.len g)) "connection"))
(check-sat)
